YES 1.541
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| (((==) :: (Eq a, Eq b) => (a,b) -> (a,b) -> Bool) :: (Eq a, Eq b) => (a,b) -> (a,b) -> Bool) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| (((==) :: (Eq b, Eq a) => (b,a) -> (b,a) -> Bool) :: (Eq a, Eq b) => (b,a) -> (b,a) -> Bool) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| ((==) :: (Eq b, Eq a) => (a,b) -> (a,b) -> Bool) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xv1800), Succ(xv401000)) → new_primPlusNat(xv1800, xv401000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xv1800), Succ(xv401000)) → new_primPlusNat(xv1800, xv401000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xv30100), Succ(xv40100)) → new_primMulNat(xv30100, Succ(xv40100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xv30100), Succ(xv40100)) → new_primMulNat(xv30100, Succ(xv40100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xv3000), Succ(xv4000)) → new_primEqNat(xv3000, xv4000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xv3000), Succ(xv4000)) → new_primEqNat(xv3000, xv4000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_esEs(@2(xv30, xv31), @2(xv40, xv41), app(app(ty_@2, ba), bb), bc) → new_esEs(xv30, xv40, ba, bb)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), app(app(app(ty_@3, gb), gc), gd)), ed), bc) → new_esEs1(xv301, xv401, gb, gc, gd)
new_esEs(@2(Left(xv300), xv31), @2(Left(xv400), xv41), app(app(ty_Either, app(app(ty_Either, bg), bh)), bf), bc) → new_esEs0(xv300, xv400, bg, bh)
new_esEs(@2(xv30, xv31), @2(xv40, xv41), bcc, app(ty_[], bdc)) → new_esEs2(xv31, xv41, bdc)
new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, app(app(app(ty_@3, gb), gc), gd), ed) → new_esEs1(xv301, xv401, gb, gc, gd)
new_esEs(@2(Just(xv300), xv31), @2(Just(xv400), xv41), app(ty_Maybe, app(app(app(ty_@3, bbf), bbg), bbh)), bc) → new_esEs1(xv300, xv400, bbf, bbg, bbh)
new_esEs(@2(Left(xv300), xv31), @2(Left(xv400), xv41), app(app(ty_Either, app(ty_Maybe, ce)), bf), bc) → new_esEs3(xv300, xv400, ce)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(ty_[], fb)), ec), ed), bc) → new_esEs2(xv300, xv400, fb)
new_esEs3(Just(xv300), Just(xv400), app(app(ty_Either, bbd), bbe)) → new_esEs0(xv300, xv400, bbd, bbe)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(ty_@2, ea), eb)), ec), ed), bc) → new_esEs(xv300, xv400, ea, eb)
new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, ec, app(app(app(ty_@3, hc), hd), he)) → new_esEs1(xv302, xv402, hc, hd, he)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(app(ty_@3, eg), eh), fa)), ec), ed), bc) → new_esEs1(xv300, xv400, eg, eh, fa)
new_esEs(@2(Left(xv300), xv31), @2(Left(xv400), xv41), app(app(ty_Either, app(app(app(ty_@3, ca), cb), cc)), bf), bc) → new_esEs1(xv300, xv400, ca, cb, cc)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), app(ty_[], ge)), ed), bc) → new_esEs2(xv301, xv401, ge)
new_esEs(@2(xv30, xv31), @2(xv40, xv41), bcc, app(app(ty_Either, bcf), bcg)) → new_esEs0(xv31, xv41, bcf, bcg)
new_esEs(@2(Right(xv300), xv31), @2(Right(xv400), xv41), app(app(ty_Either, cf), app(app(app(ty_@3, dd), de), df)), bc) → new_esEs1(xv300, xv400, dd, de, df)
new_esEs0(Left(xv300), Left(xv400), app(app(ty_@2, bd), be), bf) → new_esEs(xv300, xv400, bd, be)
new_esEs(@2(Just(xv300), xv31), @2(Just(xv400), xv41), app(ty_Maybe, app(app(ty_@2, bbb), bbc)), bc) → new_esEs(xv300, xv400, bbb, bbc)
new_esEs(@2(Just(xv300), xv31), @2(Just(xv400), xv41), app(ty_Maybe, app(app(ty_Either, bbd), bbe)), bc) → new_esEs0(xv300, xv400, bbd, bbe)
new_esEs0(Right(xv300), Right(xv400), cf, app(ty_[], dg)) → new_esEs2(xv300, xv400, dg)
new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, ec, app(app(ty_@2, gg), gh)) → new_esEs(xv302, xv402, gg, gh)
new_esEs(@2(Just(xv300), xv31), @2(Just(xv400), xv41), app(ty_Maybe, app(ty_Maybe, bcb)), bc) → new_esEs3(xv300, xv400, bcb)
new_esEs0(Right(xv300), Right(xv400), cf, app(app(ty_Either, db), dc)) → new_esEs0(xv300, xv400, db, dc)
new_esEs3(Just(xv300), Just(xv400), app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs1(xv300, xv400, bbf, bbg, bbh)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), app(ty_Maybe, gf)), ed), bc) → new_esEs3(xv301, xv401, gf)
new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_Either, ee), ef), ec, ed) → new_esEs0(xv300, xv400, ee, ef)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), ec), app(ty_[], hf)), bc) → new_esEs2(xv302, xv402, hf)
new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_Maybe, fc), ec, ed) → new_esEs3(xv300, xv400, fc)
new_esEs0(Left(xv300), Left(xv400), app(ty_[], cd), bf) → new_esEs2(xv300, xv400, cd)
new_esEs2(:(xv300, xv301), :(xv400, xv401), app(ty_[], bag)) → new_esEs2(xv300, xv400, bag)
new_esEs(@2(Right(xv300), xv31), @2(Right(xv400), xv41), app(app(ty_Either, cf), app(app(ty_@2, cg), da)), bc) → new_esEs(xv300, xv400, cg, da)
new_esEs(@2(xv30, xv31), @2(xv40, xv41), bcc, app(app(ty_@2, bcd), bce)) → new_esEs(xv31, xv41, bcd, bce)
new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_[], fb), ec, ed) → new_esEs2(xv300, xv400, fb)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], app(ty_Maybe, bah)), bc) → new_esEs3(xv300, xv400, bah)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), ec), app(app(ty_Either, ha), hb)), bc) → new_esEs0(xv302, xv402, ha, hb)
new_esEs(@2(Left(xv300), xv31), @2(Left(xv400), xv41), app(app(ty_Either, app(app(ty_@2, bd), be)), bf), bc) → new_esEs(xv300, xv400, bd, be)
new_esEs2(:(xv300, xv301), :(xv400, xv401), app(ty_Maybe, bah)) → new_esEs3(xv300, xv400, bah)
new_esEs3(Just(xv300), Just(xv400), app(ty_[], bca)) → new_esEs2(xv300, xv400, bca)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), app(app(ty_@2, ff), fg)), ed), bc) → new_esEs(xv301, xv401, ff, fg)
new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, app(app(ty_@2, ff), fg), ed) → new_esEs(xv301, xv401, ff, fg)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), ec), app(app(ty_@2, gg), gh)), bc) → new_esEs(xv302, xv402, gg, gh)
new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, app(ty_Maybe, gf), ed) → new_esEs3(xv301, xv401, gf)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), ec), app(ty_Maybe, hg)), bc) → new_esEs3(xv302, xv402, hg)
new_esEs0(Left(xv300), Left(xv400), app(ty_Maybe, ce), bf) → new_esEs3(xv300, xv400, ce)
new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, ec, app(ty_[], hf)) → new_esEs2(xv302, xv402, hf)
new_esEs0(Left(xv300), Left(xv400), app(app(ty_Either, bg), bh), bf) → new_esEs0(xv300, xv400, bg, bh)
new_esEs(@2(xv30, xv31), @2(xv40, xv41), bcc, app(ty_Maybe, bdd)) → new_esEs3(xv31, xv41, bdd)
new_esEs(@2(Left(xv300), xv31), @2(Left(xv400), xv41), app(app(ty_Either, app(ty_[], cd)), bf), bc) → new_esEs2(xv300, xv400, cd)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(ty_Either, ee), ef)), ec), ed), bc) → new_esEs0(xv300, xv400, ee, ef)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], app(app(ty_@2, hh), baa)), bc) → new_esEs(xv300, xv400, hh, baa)
new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, app(ty_[], ge), ed) → new_esEs2(xv301, xv401, ge)
new_esEs(@2(xv30, xv31), @2(xv40, xv41), bcc, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs1(xv31, xv41, bch, bda, bdb)
new_esEs2(:(xv300, xv301), :(xv400, xv401), app(app(app(ty_@3, bad), bae), baf)) → new_esEs1(xv300, xv400, bad, bae, baf)
new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(app(ty_@3, eg), eh), fa), ec, ed) → new_esEs1(xv300, xv400, eg, eh, fa)
new_esEs2(:(xv300, xv301), :(xv400, xv401), app(app(ty_Either, bab), bac)) → new_esEs0(xv300, xv400, bab, bac)
new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, ec, app(ty_Maybe, hg)) → new_esEs3(xv302, xv402, hg)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], bba), bc) → new_esEs2(xv301, xv401, bba)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], app(app(app(ty_@3, bad), bae), baf)), bc) → new_esEs1(xv300, xv400, bad, bae, baf)
new_esEs(@2(Right(xv300), xv31), @2(Right(xv400), xv41), app(app(ty_Either, cf), app(ty_Maybe, dh)), bc) → new_esEs3(xv300, xv400, dh)
new_esEs(@2(Right(xv300), xv31), @2(Right(xv400), xv41), app(app(ty_Either, cf), app(app(ty_Either, db), dc)), bc) → new_esEs0(xv300, xv400, db, dc)
new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, app(app(ty_Either, fh), ga), ed) → new_esEs0(xv301, xv401, fh, ga)
new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, ec, app(app(ty_Either, ha), hb)) → new_esEs0(xv302, xv402, ha, hb)
new_esEs2(:(xv300, xv301), :(xv400, xv401), bba) → new_esEs2(xv301, xv401, bba)
new_esEs3(Just(xv300), Just(xv400), app(ty_Maybe, bcb)) → new_esEs3(xv300, xv400, bcb)
new_esEs2(:(xv300, xv301), :(xv400, xv401), app(app(ty_@2, hh), baa)) → new_esEs(xv300, xv400, hh, baa)
new_esEs3(Just(xv300), Just(xv400), app(app(ty_@2, bbb), bbc)) → new_esEs(xv300, xv400, bbb, bbc)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(ty_Maybe, fc)), ec), ed), bc) → new_esEs3(xv300, xv400, fc)
new_esEs0(Right(xv300), Right(xv400), cf, app(ty_Maybe, dh)) → new_esEs3(xv300, xv400, dh)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), app(app(ty_Either, fh), ga)), ed), bc) → new_esEs0(xv301, xv401, fh, ga)
new_esEs(@2(Just(xv300), xv31), @2(Just(xv400), xv41), app(ty_Maybe, app(ty_[], bca)), bc) → new_esEs2(xv300, xv400, bca)
new_esEs(@2(Right(xv300), xv31), @2(Right(xv400), xv41), app(app(ty_Either, cf), app(ty_[], dg)), bc) → new_esEs2(xv300, xv400, dg)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), ec), app(app(app(ty_@3, hc), hd), he)), bc) → new_esEs1(xv302, xv402, hc, hd, he)
new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_@2, ea), eb), ec, ed) → new_esEs(xv300, xv400, ea, eb)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], app(ty_[], bag)), bc) → new_esEs2(xv300, xv400, bag)
new_esEs0(Right(xv300), Right(xv400), cf, app(app(ty_@2, cg), da)) → new_esEs(xv300, xv400, cg, da)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], app(app(ty_Either, bab), bac)), bc) → new_esEs0(xv300, xv400, bab, bac)
new_esEs0(Left(xv300), Left(xv400), app(app(app(ty_@3, ca), cb), cc), bf) → new_esEs1(xv300, xv400, ca, cb, cc)
new_esEs0(Right(xv300), Right(xv400), cf, app(app(app(ty_@3, dd), de), df)) → new_esEs1(xv300, xv400, dd, de, df)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs2(:(xv300, xv301), :(xv400, xv401), app(app(ty_@2, hh), baa)) → new_esEs(xv300, xv400, hh, baa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(xv300), Just(xv400), app(app(ty_@2, bbb), bbc)) → new_esEs(xv300, xv400, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(:(xv300, xv301), :(xv400, xv401), app(app(app(ty_@3, bad), bae), baf)) → new_esEs1(xv300, xv400, bad, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Just(xv300), Just(xv400), app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs1(xv300, xv400, bbf, bbg, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(:(xv300, xv301), :(xv400, xv401), app(ty_Maybe, bah)) → new_esEs3(xv300, xv400, bah)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(xv300), Just(xv400), app(ty_Maybe, bcb)) → new_esEs3(xv300, xv400, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(:(xv300, xv301), :(xv400, xv401), app(app(ty_Either, bab), bac)) → new_esEs0(xv300, xv400, bab, bac)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(xv300), Just(xv400), app(app(ty_Either, bbd), bbe)) → new_esEs0(xv300, xv400, bbd, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(xv300), Just(xv400), app(ty_[], bca)) → new_esEs2(xv300, xv400, bca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(xv30, xv31), @2(xv40, xv41), app(app(ty_@2, ba), bb), bc) → new_esEs(xv30, xv40, ba, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(ty_@2, ea), eb)), ec), ed), bc) → new_esEs(xv300, xv400, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(Just(xv300), xv31), @2(Just(xv400), xv41), app(ty_Maybe, app(app(ty_@2, bbb), bbc)), bc) → new_esEs(xv300, xv400, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(Right(xv300), xv31), @2(Right(xv400), xv41), app(app(ty_Either, cf), app(app(ty_@2, cg), da)), bc) → new_esEs(xv300, xv400, cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(xv30, xv31), @2(xv40, xv41), bcc, app(app(ty_@2, bcd), bce)) → new_esEs(xv31, xv41, bcd, bce)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@2(Left(xv300), xv31), @2(Left(xv400), xv41), app(app(ty_Either, app(app(ty_@2, bd), be)), bf), bc) → new_esEs(xv300, xv400, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), app(app(ty_@2, ff), fg)), ed), bc) → new_esEs(xv301, xv401, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), ec), app(app(ty_@2, gg), gh)), bc) → new_esEs(xv302, xv402, gg, gh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], app(app(ty_@2, hh), baa)), bc) → new_esEs(xv300, xv400, hh, baa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), app(app(app(ty_@3, gb), gc), gd)), ed), bc) → new_esEs1(xv301, xv401, gb, gc, gd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(Just(xv300), xv31), @2(Just(xv400), xv41), app(ty_Maybe, app(app(app(ty_@3, bbf), bbg), bbh)), bc) → new_esEs1(xv300, xv400, bbf, bbg, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(app(ty_@3, eg), eh), fa)), ec), ed), bc) → new_esEs1(xv300, xv400, eg, eh, fa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(Left(xv300), xv31), @2(Left(xv400), xv41), app(app(ty_Either, app(app(app(ty_@3, ca), cb), cc)), bf), bc) → new_esEs1(xv300, xv400, ca, cb, cc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(Right(xv300), xv31), @2(Right(xv400), xv41), app(app(ty_Either, cf), app(app(app(ty_@3, dd), de), df)), bc) → new_esEs1(xv300, xv400, dd, de, df)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(xv30, xv31), @2(xv40, xv41), bcc, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs1(xv31, xv41, bch, bda, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], app(app(app(ty_@3, bad), bae), baf)), bc) → new_esEs1(xv300, xv400, bad, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), ec), app(app(app(ty_@3, hc), hd), he)), bc) → new_esEs1(xv302, xv402, hc, hd, he)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(Left(xv300), xv31), @2(Left(xv400), xv41), app(app(ty_Either, app(ty_Maybe, ce)), bf), bc) → new_esEs3(xv300, xv400, ce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(Just(xv300), xv31), @2(Just(xv400), xv41), app(ty_Maybe, app(ty_Maybe, bcb)), bc) → new_esEs3(xv300, xv400, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), app(ty_Maybe, gf)), ed), bc) → new_esEs3(xv301, xv401, gf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], app(ty_Maybe, bah)), bc) → new_esEs3(xv300, xv400, bah)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), ec), app(ty_Maybe, hg)), bc) → new_esEs3(xv302, xv402, hg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(xv30, xv31), @2(xv40, xv41), bcc, app(ty_Maybe, bdd)) → new_esEs3(xv31, xv41, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@2(Right(xv300), xv31), @2(Right(xv400), xv41), app(app(ty_Either, cf), app(ty_Maybe, dh)), bc) → new_esEs3(xv300, xv400, dh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(ty_Maybe, fc)), ec), ed), bc) → new_esEs3(xv300, xv400, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(Left(xv300), xv31), @2(Left(xv400), xv41), app(app(ty_Either, app(app(ty_Either, bg), bh)), bf), bc) → new_esEs0(xv300, xv400, bg, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(xv30, xv31), @2(xv40, xv41), bcc, app(app(ty_Either, bcf), bcg)) → new_esEs0(xv31, xv41, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@2(Just(xv300), xv31), @2(Just(xv400), xv41), app(ty_Maybe, app(app(ty_Either, bbd), bbe)), bc) → new_esEs0(xv300, xv400, bbd, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), ec), app(app(ty_Either, ha), hb)), bc) → new_esEs0(xv302, xv402, ha, hb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(ty_Either, ee), ef)), ec), ed), bc) → new_esEs0(xv300, xv400, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(Right(xv300), xv31), @2(Right(xv400), xv41), app(app(ty_Either, cf), app(app(ty_Either, db), dc)), bc) → new_esEs0(xv300, xv400, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), app(app(ty_Either, fh), ga)), ed), bc) → new_esEs0(xv301, xv401, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], app(app(ty_Either, bab), bac)), bc) → new_esEs0(xv300, xv400, bab, bac)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(xv30, xv31), @2(xv40, xv41), bcc, app(ty_[], bdc)) → new_esEs2(xv31, xv41, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(ty_[], fb)), ec), ed), bc) → new_esEs2(xv300, xv400, fb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), app(ty_[], ge)), ed), bc) → new_esEs2(xv301, xv401, ge)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, fd), ec), app(ty_[], hf)), bc) → new_esEs2(xv302, xv402, hf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(Left(xv300), xv31), @2(Left(xv400), xv41), app(app(ty_Either, app(ty_[], cd)), bf), bc) → new_esEs2(xv300, xv400, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], bba), bc) → new_esEs2(xv301, xv401, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(Right(xv300), xv31), @2(Right(xv400), xv41), app(app(ty_Either, cf), app(ty_[], dg)), bc) → new_esEs2(xv300, xv400, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(Just(xv300), xv31), @2(Just(xv400), xv41), app(ty_Maybe, app(ty_[], bca)), bc) → new_esEs2(xv300, xv400, bca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv400, xv401), xv41), app(ty_[], app(ty_[], bag)), bc) → new_esEs2(xv300, xv400, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, ec, app(app(ty_@2, gg), gh)) → new_esEs(xv302, xv402, gg, gh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, app(app(ty_@2, ff), fg), ed) → new_esEs(xv301, xv401, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_@2, ea), eb), ec, ed) → new_esEs(xv300, xv400, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Left(xv300), Left(xv400), app(app(ty_@2, bd), be), bf) → new_esEs(xv300, xv400, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Right(xv300), Right(xv400), cf, app(app(ty_@2, cg), da)) → new_esEs(xv300, xv400, cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, app(app(app(ty_@3, gb), gc), gd), ed) → new_esEs1(xv301, xv401, gb, gc, gd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, ec, app(app(app(ty_@3, hc), hd), he)) → new_esEs1(xv302, xv402, hc, hd, he)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(app(ty_@3, eg), eh), fa), ec, ed) → new_esEs1(xv300, xv400, eg, eh, fa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_Maybe, fc), ec, ed) → new_esEs3(xv300, xv400, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, app(ty_Maybe, gf), ed) → new_esEs3(xv301, xv401, gf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, ec, app(ty_Maybe, hg)) → new_esEs3(xv302, xv402, hg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_Either, ee), ef), ec, ed) → new_esEs0(xv300, xv400, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, app(app(ty_Either, fh), ga), ed) → new_esEs0(xv301, xv401, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, ec, app(app(ty_Either, ha), hb)) → new_esEs0(xv302, xv402, ha, hb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_[], fb), ec, ed) → new_esEs2(xv300, xv400, fb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, ec, app(ty_[], hf)) → new_esEs2(xv302, xv402, hf)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs1(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), fd, app(ty_[], ge), ed) → new_esEs2(xv301, xv401, ge)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(Left(xv300), Left(xv400), app(app(app(ty_@3, ca), cb), cc), bf) → new_esEs1(xv300, xv400, ca, cb, cc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Right(xv300), Right(xv400), cf, app(app(app(ty_@3, dd), de), df)) → new_esEs1(xv300, xv400, dd, de, df)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(Left(xv300), Left(xv400), app(ty_Maybe, ce), bf) → new_esEs3(xv300, xv400, ce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Right(xv300), Right(xv400), cf, app(ty_Maybe, dh)) → new_esEs3(xv300, xv400, dh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(Right(xv300), Right(xv400), cf, app(app(ty_Either, db), dc)) → new_esEs0(xv300, xv400, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(Left(xv300), Left(xv400), app(app(ty_Either, bg), bh), bf) → new_esEs0(xv300, xv400, bg, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Right(xv300), Right(xv400), cf, app(ty_[], dg)) → new_esEs2(xv300, xv400, dg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(Left(xv300), Left(xv400), app(ty_[], cd), bf) → new_esEs2(xv300, xv400, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(:(xv300, xv301), :(xv400, xv401), app(ty_[], bag)) → new_esEs2(xv300, xv400, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(:(xv300, xv301), :(xv400, xv401), bba) → new_esEs2(xv301, xv401, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3